(set-logic QF_BV)
(declare-fun _substvar_66_ () (_ BitVec 32))
(declare-fun _substvar_89_ () (_ BitVec 8))
(declare-fun _substvar_91_ () (_ BitVec 32))
(declare-fun _substvar_65_ () (_ BitVec 8))
(declare-fun _substvar_87_ () (_ BitVec 32))
(declare-fun _substvar_85_ () (_ BitVec 32))
(assert (= _substvar_66_ ((_ sign_extend 24) _substvar_65_)))
(assert (= _substvar_85_ _substvar_66_))
(assert (= _substvar_87_ _substvar_85_))
(assert (= _substvar_89_ ((_ extract 7 0) _substvar_87_)))
(assert (= _substvar_91_ ((_ sign_extend 24) _substvar_89_)))
(assert (= (_ bv0 32) (bvadd _substvar_91_ ((_ extract 31 0) (_ bv24 64)))))
(check-sat)
(exit)
